Field of the Invention
The present invention relates to techniques for verifying the correctness of an integrated circuit design, and in particular to accelerating coverage convergence using symbolic properties together with a directed graph that represents a reason a coverage point cannot be hit after symbolic simulation.
Related Art
Integrated circuit designs have increasingly higher complexity. This complexity makes determining the correctness of the design both difficult and resource intensive. To verify the correctness of a design, a verification tool typically applies stimuli to the design under verification (DUV). In general, many stimuli and simulation runs are needed to achieve a reasonable coverage of the behavior of the DUV. The simulation outputs of the DUV can be compared to expected outputs to determine whether the design is providing the desired functionality.
Coverage is a key metric that measures the quality and project completeness in the functional verification of the design. Types of coverage targets can be characterized as either functional coverage targets or code coverage targets. In a functional coverage target, a user wants some scenario to happen in the design. For example, the user wants signal A to have value X at the same time that signal B has value Y. In contrast, the code coverage target can include branch (if, case) statement, and line coverage. These types of coverage targets are well known and therefore not described in further detail.
Note that conventional simulations cannot generate such scenario information—hence the need for the user to specify coverage targets in a test bench. For example, FIG. 1 illustrates a conventional environment for a verification tool with an open loop, coverage convergence technique. In this environment, variables 101 of the hardware description language (HDL) code (typically in a register transfer level (RTL) format) of a design 103 are identified. In one embodiment, variables 101 are the input variables of design 103. In another embodiment, variables 101 are the input variables of specific starting points in design 103. After identification, randomized values 102 (i.e. stimuli) for variables 101 can be generated.
These randomized values 102 as well as user-provided coverage targets 104 can be provided to design 103 for simulation. In one embodiment, these simulations can be performed using a test bench 106 and design 103 is then typically referred to as a device-under-test (DUT). In another embodiment, the randomized values 102 can also be generated by test bench 106. The simulation results can be analyzed using functional verification and then provided to the user as coverage results 105.
Conventional functional verification uses constrained random simulation, which enables users to go from 0 to 80-90% coverage by automatically creating thousands of tests (i.e. different stimuli). However, getting the remaining 10-20% coverage is a very time consuming and difficult manual process. Typically, this process requires that verification engineers work with design engineers to analyze the coverage obtained so far, identify coverage holes, determine the reasons for not reaching the missing coverage targets, and write new tests to hit the missing targets and achieve coverage convergence. Unfortunately, this coverage convergence phase of verification can take up to 30% of the overall chip development cycle.
Previous techniques for automatically reaching the missing coverage targets have encountered severe scalability problems and require extensive modifications to existing verification tools. One such technique relies on randomly changing paths based on symbolic properties with the goal of executing new, previously un-explored branches in the code.
A method for increasing coverage convergence during verification of a design for an integrated circuit is provided is disclosed in U.S. Patent Application 20120266118 entitled Accelerating Coverage Convergence Using Symbolic Properties, filed Apr. 14, 2011, the disclosure of which is incorporated herein by reference. In this method, multiple simulation runs are performed. Symbolic variables and symbolic expressions can be generated for the variables and the variable expressions in the hardware code of the design and a test bench. Exemplary hardware code includes the hardware description language (HDL) code and/or the hardware verification language (HVL) code and/or a stimulus graph description. Symbolic properties, which are derived from propagating the symbolic variables and symbolic expressions through the design and the test bench during the multiple simulation runs, can be collected. Coverage information from the multiple simulation runs can be analyzed to identify coverage points to be targeted. At this point, for each identified coverage point, the constraints resulting from the collected symbolic properties can be solved to generate directed stimuli for the design. These directed stimuli can increase the coverage convergence.
However, no tool has a concise way to display cause-effect data from a symbolic simulation.